home *** CD-ROM | disk | FTP | other *** search
/ Aminet 37 / Aminet 37 (2000)(Schatztruhe)[!][Jun 2000].iso / Aminet / dev / lang / sofa.lha / sofa / smalleiffel / lib_se / class_invariant.e < prev    next >
Text File  |  2000-03-25  |  7KB  |  190 lines
  1. --          This file is part of SmallEiffel The GNU Eiffel Compiler.
  2. --          Copyright (C) 1994-98 LORIA - UHP - CRIN - INRIA - FRANCE
  3. --            Dominique COLNET and Suzanne COLLIN - colnet@loria.fr
  4. --                       http://SmallEiffel.loria.fr
  5. -- SmallEiffel is  free  software;  you can  redistribute it and/or modify it
  6. -- under the terms of the GNU General Public License as published by the Free
  7. -- Software  Foundation;  either  version  2, or (at your option)  any  later
  8. -- version. SmallEiffel is distributed in the hope that it will be useful,but
  9. -- WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
  10. -- or  FITNESS FOR A PARTICULAR PURPOSE.   See the GNU General Public License
  11. -- for  more  details.  You  should  have  received a copy of the GNU General
  12. -- Public  License  along  with  SmallEiffel;  see the file COPYING.  If not,
  13. -- write to the  Free Software Foundation, Inc., 59 Temple Place - Suite 330,
  14. -- Boston, MA 02111-1307, USA.
  15. --
  16. class CLASS_INVARIANT
  17.    --
  18.    -- To store a `class invariant'.
  19.    --
  20.  
  21. inherit ASSERTION_LIST redefine pretty_print end;
  22.  
  23. creation make, make_runnable
  24.  
  25. feature
  26.  
  27.    name: STRING is
  28.       do
  29.          Result := fz_invariant;
  30.       end;
  31.  
  32.    pretty_print is
  33.       local
  34.          indent_level, i: INTEGER;
  35.       do 
  36.      indent_level := fmt.indent_level;
  37.          fmt.set_indent_level(0);
  38.          if not fmt.zen_mode then
  39.             fmt.skip(1);
  40.          end;
  41.          fmt.keyword(name);
  42.          if header_comment /= Void then
  43.             header_comment.pretty_print;
  44.          end;
  45.          if list /= Void then
  46.             from
  47.                i := 1;
  48.             until
  49.                i > list.upper
  50.             loop
  51.                fmt.set_indent_level(1);
  52.                fmt.indent;
  53.                if not fmt.zen_mode then
  54.                   fmt.skip(1);
  55.                end;
  56.                fmt.set_semi_colon_flag(true);
  57.                list.item(i).pretty_print;
  58.                i := i + 1;
  59.             end;
  60.          end;
  61.      fmt.set_indent_level(indent_level);
  62.       end;
  63.  
  64.    short(bc: BASE_CLASS) is
  65.       local
  66.          i: INTEGER;
  67.       do
  68.          bc.header_comment_for(Current);
  69.          short_print.hook_or("hook811","invariant%N");
  70.          if header_comment = Void then
  71.             short_print.hook_or("hook812","");
  72.          else
  73.             short_print.hook_or("hook813","");
  74.             header_comment.short("hook814","   -- ","hook815","%N");
  75.             short_print.hook_or("hook816","");
  76.          end;
  77.          if list = Void then
  78.             short_print.hook_or("hook817","");
  79.          else
  80.             short_print.hook_or("hook818","");
  81.             from
  82.                i := 1;
  83.             until
  84.                i = list.upper
  85.             loop
  86.                list.item(i).short("hook819","   ", -- before each assertion
  87.                                   "hook820","", -- no tag
  88.                                   "hook821","", -- before tag
  89.                                   "hook822",": ", -- after tag
  90.                                   "hook823","", -- no expression
  91.                                   "hook824","", -- before expression
  92.                                   "hook825",";", -- after expression except last
  93.                                   "hook826","%N", -- no comment
  94.                                   "hook827","", -- before comment
  95.                                   "hook828"," -- ", -- comment begin line
  96.                                   "hook829","%N", -- comment end of line
  97.                                   "hook830","", -- after comment
  98.                                   "hook831",""); -- end of each assertion
  99.  
  100.                i := i + 1;
  101.             end;
  102.             list.item(i).short("hook819","   ", -- before each assertion
  103.                                "hook820","", -- no tag
  104.                                "hook821","", -- before tag
  105.                                "hook822",": ", -- after tag
  106.                                "hook823","", -- no expression
  107.                                "hook824","", -- before expression
  108.                                "hook832",";", -- after last expression
  109.                                "hook826","%N", -- no comment
  110.                                "hook827","", -- before comment
  111.                                "hook828"," -- ", -- comment begin line
  112.                                "hook829","%N", -- comment end of line
  113.                                "hook830","", -- after comment
  114.                                "hook831","");
  115.             short_print.hook_or("hook833","");
  116.          end;
  117.          short_print.hook_or("hook834","");
  118.       ensure
  119.          fmt.indent_level = old fmt.indent_level;
  120.       end;
  121.  
  122. feature {NONE}
  123.  
  124.    check_assertion_mode: STRING is
  125.       do
  126.          Result := "inv";
  127.       end;
  128.  
  129. feature {RUN_CLASS}
  130.  
  131.    c_define is
  132.          -- Define C function to check invariant.
  133.       require
  134.          run_control.invariant_check;
  135.          current_type /= Void;
  136.          run_class.at_run_time;
  137.          small_eiffel.is_ready;
  138.          cpp.on_c
  139.       local
  140.          id: INTEGER;
  141.       do
  142.          id := current_type.id;
  143.          -- The invariant frame descriptor :
  144.          c_code.copy("se_frame_descriptor se_ifd");
  145.          id.append_in(c_code);
  146.          cpp.put_extern7(c_code);
  147.          c_code.copy("{%"Class invariant of ");
  148.          c_code.append(current_type.run_time_mark);
  149.          c_code.append("%",1,0,%"");
  150.          c_frame_descriptor_format.clear;
  151.          current_type.c_frame_descriptor;
  152.          c_code.append(c_frame_descriptor_format);
  153.          c_code.append("%",1};%N");
  154.          cpp.put_string(c_code);
  155.          -- The function :
  156.          c_code.clear;
  157.          c_code.extend('T');
  158.          id.append_in(c_code);
  159.          c_code.extend('*');
  160.          c_code.append(fz_se_i);
  161.          id.append_in(c_code);
  162.          c_code.append("(se_dump_stack*caller,T");
  163.          id.append_in(c_code);
  164.          c_code.append("*C)");
  165.          cpp.put_c_heading(c_code);
  166.          cpp.swap_on_c;
  167.          c_code.copy("se_dump_stack ds;%Nds.fd=&se_ifd");
  168.          id.append_in(c_code);
  169.          c_code.append(";%Nds.current=((void**)&C);%N");
  170.          cpp.put_string(c_code);
  171.          cpp.put_position_in_ds(start_position);
  172.          cpp.put_string(
  173.             "ds.caller=caller;%N%
  174.             %se_dst=&ds;%N");
  175.          compile_to_c;
  176.          cpp.put_string("se_dst=caller;%Nreturn C;%N}%N");
  177.       ensure
  178.          cpp.on_c
  179.       end;
  180.  
  181. feature {NONE}
  182.  
  183.    c_code: STRING is
  184.       once
  185.          !!Result.make(128);
  186.       end;
  187.  
  188. end -- CLASS_INVARIANT
  189.  
  190.